'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f(f(g(x1))) -> g(f(x1))} Details: We have computed the following set of weak (innermost) dependency pairs: { g^#(c(x1)) -> c_0(g^#(f(c(x1)))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1))))) , g^#(g(x1)) -> c_2(g^#(f(g(x1)))) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} The usable rules are: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f(f(g(x1))) -> g(f(x1))} The estimated dependency graph contains the following edges: {g^#(c(x1)) -> c_0(g^#(f(c(x1))))} ==> {g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} {g^#(g(x1)) -> c_2(g^#(f(g(x1))))} ==> {g^#(g(x1)) -> c_2(g^#(f(g(x1))))} {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} ==> {g^#(g(x1)) -> c_2(g^#(f(g(x1))))} {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} ==> {g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} We consider the following path(s): 1) { f^#(f(g(x1))) -> c_3(g^#(f(x1))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} The usable rules for this path are the following: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f^#(f(g(x1))) -> c_3(g^#(f(x1))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Details: We apply the weight gap principle, strictly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [0] f(x1) = [1] x1 + [0] g^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] c_1(x1) = [1] x1 + [8] c_2(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [9] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f(f(g(x1))) -> g(f(x1))} and weakly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(f(g(x1))) -> g(f(x1))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [2] f(x1) = [1] x1 + [8] g^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] c_1(x1) = [1] x1 + [0] c_2(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [8] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { c_0(2) -> 2 , g^#_0(2) -> 4 , f^#_0(2) -> 8} 2) { g^#(c(x1)) -> c_0(g^#(f(c(x1)))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} The usable rules for this path are the following: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1)))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Details: We apply the weight gap principle, strictly orienting the rules {f(f(g(x1))) -> g(f(x1))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(f(g(x1))) -> g(f(x1))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [15] f(x1) = [1] x1 + [15] g^#(x1) = [1] x1 + [3] c_0(x1) = [1] x1 + [7] c_1(x1) = [1] x1 + [2] c_2(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1)))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Weak Rules: {f(f(g(x1))) -> g(f(x1))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1)))) , g^#(f(c(x1))) -> c_1(g^#(f(f(c(x1)))))} Weak Rules: {f(f(g(x1))) -> g(f(x1))} Details: The problem is Match-bounded by 2. The enriched problem is compatible with the following automaton: { c_0(2) -> 2 , c_1(2) -> 5 , c_2(2) -> 9 , f_1(5) -> 4 , f_2(8) -> 7 , f_2(9) -> 8 , g^#_0(2) -> 1 , g^#_1(4) -> 3 , g^#_2(7) -> 6 , c_0_1(3) -> 1 , c_1_2(6) -> 3} 3) { f^#(f(g(x1))) -> c_3(g^#(f(x1))) , g^#(g(x1)) -> c_2(g^#(f(g(x1))))} The usable rules for this path are the following: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f(f(g(x1))) -> g(f(x1))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1))) , g^#(g(x1)) -> c_2(g^#(f(g(x1))))} Details: We apply the weight gap principle, strictly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: Interpretation Functions: g(x1) = [1] x1 + [1] c(x1) = [1] x1 + [0] f(x1) = [1] x1 + [0] g^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [2] f^#(x1) = [1] x1 + [4] c_3(x1) = [1] x1 + [3] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f(f(g(x1))) -> g(f(x1))} and weakly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(f(g(x1))) -> g(f(x1))} Details: Interpretation Functions: g(x1) = [1] x1 + [1] c(x1) = [1] x1 + [0] f(x1) = [1] x1 + [8] g^#(x1) = [1] x1 + [7] c_0(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [1] x1 + [0] f^#(x1) = [1] x1 + [6] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(g(x1)) -> c_2(g^#(f(g(x1))))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(g(x1)) -> c_2(g^#(f(g(x1))))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { c_0(2) -> 2 , g^#_0(2) -> 4 , f^#_0(2) -> 8} 4) {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} The usable rules for this path are the following: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: We apply the weight gap principle, strictly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [0] f(x1) = [1] x1 + [0] g^#(x1) = [1] x1 + [0] c_0(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [1] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {f(f(g(x1))) -> g(f(x1))} and weakly orienting the rules {f^#(f(g(x1))) -> c_3(g^#(f(x1)))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(f(g(x1))) -> g(f(x1))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [8] f(x1) = [1] x1 + [8] g^#(x1) = [1] x1 + [1] c_0(x1) = [0] x1 + [0] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] f^#(x1) = [1] x1 + [9] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} Weak Rules: { f(f(g(x1))) -> g(f(x1)) , f^#(f(g(x1))) -> c_3(g^#(f(x1)))} Details: The problem is Match-bounded by 0. The enriched problem is compatible with the following automaton: { c_0(2) -> 2 , g^#_0(2) -> 4 , f^#_0(2) -> 8} 5) {g^#(c(x1)) -> c_0(g^#(f(c(x1))))} The usable rules for this path are the following: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1)))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { f(f(g(x1))) -> g(f(x1)) , g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1))))} Details: We apply the weight gap principle, strictly orienting the rules {f(f(g(x1))) -> g(f(x1))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {f(f(g(x1))) -> g(f(x1))} Details: Interpretation Functions: g(x1) = [1] x1 + [0] c(x1) = [1] x1 + [2] f(x1) = [1] x1 + [4] g^#(x1) = [1] x1 + [2] c_0(x1) = [1] x1 + [2] c_1(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] f^#(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1))))} Weak Rules: {f(f(g(x1))) -> g(f(x1))} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { g(c(x1)) -> g(f(c(x1))) , g(f(c(x1))) -> g(f(f(c(x1)))) , g(g(x1)) -> g(f(g(x1))) , g^#(c(x1)) -> c_0(g^#(f(c(x1))))} Weak Rules: {f(f(g(x1))) -> g(f(x1))} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { c_0(2) -> 2 , c_1(2) -> 7 , f_1(7) -> 6 , g^#_0(2) -> 4 , g^#_1(6) -> 5 , c_0_1(5) -> 4}